T:Type, as,bs,cs:(T List).
iseg(T; cs; as)  (b:T. (cs = append(as; cons(b; bs)))  False) 

latex

Definitions	t  T, x:A. B(x), ge(i; j), ||as||, False, top, subtype(S; T), A  B, P  Q, iseg(T; l1; l2), append(as; bs), prop{i:l}, P  Q, P  Q, P  Q
Lemmas	append wf, false wf, iseg wf, iseg length, le wf, length wf1, length-append, top wf, non neg length